\section{Auxiliary Definitions}
\subsection{Cardinality of Typings\label{ap:count}}
\begin{definition}
Let $\ActS$ be a typing, as in Table~\ref{tab:types}. The cardinality of $\ActS$, denoted $|\ActS|$, is inductively defined as follows:
\begin{align*}
|\emptyset| & = 0 \\
|\ActS', k:\ST| & = 1 + |\ActS'| \\
|\ActS', [k:\ST]| & = 1 + |\ActS'| \\
\end{align*}
\end{definition}


\section{Proofs from \S\,\ref{sec:res}}

\subsection{Proof of Theorem~\ref{th:congr}\label{app:congr}}
We repeat the statement given in Page~\pageref{th:congr} and give its proof.

\begin{theorem}[Subject Congruence] 
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ and $P \equiv Q$ then $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}$.
\end{theorem}
\begin{proof}
By induction on the derivation of $P \equiv Q$, with a case analysis on the last applied rule.

%\begin{description}
\paragraph{\bf Case $\restr{\cha}{ ( \compo{l}{h}{P})  } \equiv   \compo{l}{h}{ \restr{\cha}{P}  }$} \quad \\
We examine the left to right direction:
we show that if 
$\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{ ( \compo{l}{h}{P} ) }}{\type{\ActS}{\INT}}$ 
then 
$\judgebis{\env{\Gamma}{\Theta}}{  \compo{l}{h}{\restr{\cha}{P}  }}{\type{\ActS}{\INT}}$.
Since $\restr{\cha}{  (\compo{l}{h}{P} ) }$ is well-typed, 
by inversion on rules \rulename{t:Loc} and \rulename{t:CRes}, 
for some $\ST, \Delta'$
we have:
$$
\cfrac{
\begin{array}{c}
\Theta \vdash l:\INT' \\
\INT \sqsubseteq \INT'
\end{array}
\quad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS', \cha^-:\ST, \cha^+:\overline{\ST}}{\INT} } \quad
 h = | \ActS', \cha^-:\ST, \cha^+:\overline{\ST} |  
}{\cfrac{\judgebis{\env{\Gamma}{\Theta}}{\compo{l}{h}{P} }{ \type{\ActS', \cha^-:\ST, \cha^+:\overline{\ST}}{\INT}}} {\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{(\compo{l}{h}{P})}}{\type{\ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT }}}}
$$ 
%\jp{perhaps this is redundant:} 
Hence $ \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS', \cha^-:\ST, \cha^+:\overline{\ST}}{\INT}}$, 
where $\ActS = \ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]$.
Now, starting from $P$, and by applying first rule  \rulename{t:CRes} and then rule  \rulename{Loc} we obtain: 
$$
\cfrac
{
\cfrac{
 \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS', \cha^-:\ST, \cha^+:\overline{\ST}}{\INT} } 
}
{ 
\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT}}}
\ 
\begin{array}{c}
\Theta \vdash l:\INT' \qquad \INT \sqsubseteq \INT' \\
 h = | \ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]| 
\end{array}
}
{\judgebis{\env{\Gamma}{\Theta}}{\compo{l}{h}{\restr{\cha}{P}} }{ \type{\ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]}{\INT}}}
$$
Observe that 
$h = | \ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]| =  | \ActS', \cha^-:\ST, \cha^+:\overline{\ST}|$---bracketing does not influence $h$, i.e.,
The reasoning for the right to left direction is analogous and omitted.


\paragraph{\bf Case $P \para \nil  \equiv P $} \quad \\ 
We examine only the left to right direction; the converse direction is similar. 
We then show that if  $\judgebis{\env{\Gamma}{\Theta}}{P \para \nil }{\type{\ActS}{\INT}}$
then  $\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{\INT}}$.
 By inversion on rule \rulename{t:Par}  there exist $\Delta_1, \INT_1$ such that $$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{\INT_1}} \text{ and }  \judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}$$
with  $\ActS= \ActS_1 \cup \emptyset = \ActS_1$ and $\INT = \INT_1 \uplus \emptyset = \INT_1$ and so the thesis follows.




\paragraph{\bf Case $\restr{\cha}{P} \para Q \equiv \restr{\cha}{(P \para Q)}$ with $\cha \notin \mathsf{fc}(Q) $} \quad \\
We examine only the right to left direction; the other direction is analogous.
We show that if 
$\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{(P \para Q)}}{\type{\ActS}{\INT}}$ (with $\cha \notin \mathsf{fc}(Q)$) then 
also 
$\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{P \para Q}}{\type{\ActS}{\INT}}$.
By inversion on rules 
\rulename{t:CRes} and \rulename{t:Par}
we have:
$$
\cfrac{
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1,  \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT_1}} \qquad
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
 \qquad
 \INT = \INT_1 \addelta \INT_2}
{ \cfrac{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2, \cha^-:\ST, \cha^+:\overline{\ST} }{\INT'}}}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{(P\para Q)}}{\type{\ActS_1 \cup \ActS_2, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT }}}}
$$
where $\ActS = \ActS_1 \cup \ActS_2, [\cha^-:\ST], [\cha^+:\overline{\ST}]$.
Observe how in the inversion of rule \rulename{t:Par} we
may combine assumption 
$\cha \notin \mathsf{fc}(Q)$ with $\alpha$-conversion to infer 
$\cha \notin \mathsf{fc}(Q) \cup \mathsf{bc}(Q)$. We may then use Lemma \ref{lem:channel}  to infer 
$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1,  \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT_1}}$ and $ \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}$. Now, % and we can construct the following derivation tree
using first rule  \rulename{t:CRes} and then rule  \rulename{t:Par} we have:
 $$
\cfrac{ 
\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1,  \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT_1}}}
{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS_1, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT_1 }}}
\quad 
\begin{array}{c}
\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
\\
 \INT = \INT_1 \addelta \INT_2
\end{array}
 } 
{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}\para Q}{\type{\ActS_1 \cup \ActS_2, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT }}}
$$
%The converse is similar.

\paragraph{\bf Case $\restr{\cha}{ \nil  } \equiv \nil$ } \quad \\ This case is easily proven by appealing to rule \rulename{t:Weak}.


\paragraph{\bf Cases $P \para Q  \equiv Q \para P$ and $(P \para Q )\para R \equiv P \para (Q \para R)$} \quad \\ 
In both cases, the proof  follows by commutativity and associativity of $\cup$ and $\uplus$ (cf. Def.~\ref{d:interf}).

\paragraph{\bf Case $\restr{\cha}{\restr{\cha'}{P}} \equiv \restr{\cha'}{\restr{\cha}{P}}$} \quad \\  This case is similar to previous ones.
%\end{description}
\end{proof}


\subsection{Proof of Theorem~\ref{th:subred}\label{app:subred}}

The proof of Theorem~\ref{th:subred} relies on the following lemma that  allows to reverse typing rules. 
\begin{lemma}[Inversion Lemma] \label{lem:types} \quad \\
\begin{description}

 \item [\rulename{t:Accept}:] \label{types8} if $\judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P}{ \type{\ActS}{\INT \uplus a:\alpha_\qual}}$ then $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\alpha}{ \INT}}$;
  
 \item [\rulename{t:RepAccept}:] \label{typesrepa} if $\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P}{ \type{\ActS}{\INT \uplus a:\alpha_\quau}}$ then there exists $\INT'$ such that  $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\alpha}{ \INT'}}$;

 \item [\rulename{t:Request}:] \label{typesreq} if $\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{x}.P}{ \type{\ActS}{\INT \uplus a:\overline{\alpha}_\qual}}$ then $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\overline{\alpha}}{ \INT}}$;

 \item [\rulename{t:Close}:] \label{types9} if $\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS,k:\epsilon}{ \INT}}$ then  $\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}}$;
   
 \item [\rulename{t:Loc}:]\label{types6} if $\judgebis{\env{\Gamma}{\Theta}}{\component{l}{h}{\INT}{P} }{ \type{\ActS}{\INT}}$ then $\Theta \vdash l:\INT' $, $\judgement{\Gamma}{\Theta}{P}{\ActS}{\INT}$, $h = |\ActS|$ and $\INT \intpr \INT'$;
 
 \item [\rulename{t:Adapt}:] \label{types7} if $\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{X}}{\type{\emptyset}{ \emptyset}}$ then  $\Theta \vdash l:\INT $ and there exists $\INT'$ such that $\judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT}}}{ P}{\type{\emptyset}{ \INT' }}$;
 
 \item [\rulename{t:CRes}:] \label{types10} if $\judgement{\Gamma}{\Theta}{\restr{\cha}{P}}{\ActS, [\cha^-:\alpha], [\cha^+:\overline{\alpha}]}{\INT}$  then $\judgement{\Gamma}{\Theta}{P}{\ActS,\cha^-:\alpha, \cha^+:\overline{\alpha}}{\INT}$;
 
 \item [\rulename{t:Par}:]\label{types1} if $\judgement{\Gamma}{\Theta}{P \para  Q}{\ActS}{\INT}$ then there exists $\ActS_1, \ActS_2, \INT_1, \INT_2$  such that $\judgement{\Gamma}{\Theta}{P}{\ActS_1}{\INT_1}$,  $\judgement{\Gamma}{\Theta}{Q}{\ActS_2}{\INT_2}$, $\ActS= \ActS_1 \cup  \ActS_2$ and $\INT = \INT_1 \uplus \INT_2$;
 
 \item [\rulename{t:Thr}:]\label{typesdelout} if $\judgement{\Gamma}{\Theta}{\throw{k}{k'}.P}{\ActS, k:!(\alpha).\beta, k':\alpha}{\INT}$ then  $\judgement{\Gamma}{\Theta}{P}{\ActS, k:\beta}{\INT}$;
 
 
 \item [\rulename{t:Cat}:]\label{typesdelin} if $\judgement{\Gamma}{\Theta}{\catch{k}{x}.P}{\ActS,k?(\alpha).\beta}{\INT}$ then $\judgement{\Gamma}{\Theta}{P}{\ActS, k:\beta, x:\alpha}{\INT}$;
 
 
 \item [\rulename{t:In}:] \label{types2} if $\judgement{\Gamma}{\Theta}{\inC{k}{\widetilde{x}}.P}{\ActS,k:?(\widetilde{\tau}).\alpha}{\INT}$  then $\judgement{\Gamma, \widetilde{x}:\tilde{\tau}}{\Theta}{P}{\ActS, k:\alpha}{\INT}$ and $\Gamma \vdash \widetilde{e}:\widetilde{\tau}$;
 
 \item [\rulename{t:Out}:]\label{types3} if $\judgement{\Gamma}{\Theta}{\outC{k}{\widetilde{e}}.P}{\ActS,k:!(\widetilde{\tau}).\alpha}{\INT}$ then $\judgement{\Gamma}{\Theta}{P}{\ActS, k:!(\widetilde{\tau}).\alpha}{\INT}$;

 \item [\rulename{t:If}:] \label{types5} if $\judgement{\Gamma}{\Theta}{\ifte{e}{P}{Q}}{\ActS}{\INT}$ then $\judgement{\Gamma}{\Theta}{P}{\ActS}{\INT}$,  $\judgement{\Gamma}{\Theta}{Q}{\ActS}{\INT}$ and $\Gamma \vdash e:\mathsf{bool} $;
 
 \item [\rulename{t:Bra}:] \label{types12} if $\judgebis{\env{\Gamma}{\Theta}}{\branch{k}{n_1:P_1 \alte \dots \alte n_m:P_m}}{\type{ \ActS, k:\&\{n_1:\alpha_1, \dots , n_m:\alpha_m \}}{ \INT}}$ then there exists $\INT_1, \dots, \INT_m$ such that for all $i\in [1..m]$, $\judgebis{\env{\Gamma}{\Theta}}{P_i}{\type{\ActS, k:\alpha_i}{ \INT_i}}$;
 
 \item [\rulename{t:Sel}:]\label{types13} if $\judgebis{\env{\Gamma}{\Theta}}{\select{k}{n_i}.P}{\type{\ActS, k:\oplus\{n_1:\alpha_1, \dots, n_m:\alpha_m\}}{\INT}}$ then $i\in [1..m]$ and $\judgebis{ \env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\alpha_i}{ \INT}}$.
\end{description}
\end{lemma}
\begin{proof}
Follows directly from the definition of typing system.
\end{proof}




We repeat the statement in Page~\pageref{th:subred} and present its proof.

\begin{theorem}[Subject Reduction]
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced and $P \pired Q$ then 
 $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS'}{\INT'}}$, for some $\INT'$ and balanced $\ActS'$.
\end{theorem}


\begin{proof}
%The proof proceeds by 
By induction on the last rule applied in the reduction. %See~\ref{app:subred} for details. 
We assume that $\til{e} \downarrow \til{c}$ is a type preserving operation, for every $\til{e}$.
%\begin{description}
\paragraph{\bf Case \rulename{r:Open}} From Table~\ref{tab:semantics} we have:
\begin{multline*} 
E\big\{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}\big\} \pired  \\
E^{++}_{} \big\{\restr{\cha}{\big({C^{+}_{}\{P_1\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }\big)\big\} } 
\end{multline*}
By assumption  $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_{2}\}\big\} }{\type{\ActS}{\INT}}$
with balanced $\ActS$.
Then, by %the following derivation tree using Lemma \ref{lem:context} ($\Leftarrow$) three times,  and  
inversion on typing, using rules \rulename{t:Fill}, \rulename{t:Accept}, \rulename{t:Request}, and \rulename{t:Par} we infer
there exist $\ActS', \INT'$ such that
{%\small
\begin{equation}\label{eq:wholeopen}
\infer
{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_{2}\}\big\}}{\type{\ActS}{\INT }}}
{
\judgebis{\bullet_{\jug_0} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{ \INT }}   & 	\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_{2}\}}{\type{\ActS'}{\INT'}}}
{    \eqref{eq:typeaccept} & \eqref{eq:typerequest}
}}
\end{equation}
}
where
$ \INT' = (\INT'_1 \addelta a:\ST_\qual) \addelta (\INT'_2\addelta a:\overline{\ST}_\qual )$
%$\{ a:\ST_\qual \addelta a:\overline{\ST}_\qual \} \subseteq \INT$, 
and
\begin{equation}
\jug_0 = \Gamma; \Theta \vdash \type{\ActS'}{\INT'} \label{eq:srjug0}
\end{equation}
%Moreover,
By Lemma~\ref{lem:context},  
$\ActS' \subseteq \ActS$ and $\INT' \intpr \INT$.
Then, letting $\ActS' = \ActS'_1 \cup \ActS'_2$, 
subtree \eqref{eq:typeaccept} is as follows: %\todo[JP:]{We should explain why $\ActS$ is different from $\ActS'$}:
\begin{equation}\label{eq:typeaccept}
\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{a}{x}.P_1\}}{\type{\ActS_1'}{ \INT_1'\addelta a:\ST_\qual }}}		  
    { 
 	\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1\addelta a:\ST_\qual}} & \infer{\judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P_1}{\type{\ActS_1}{ \INT_1\addelta a:\ST_\qual  }}}
  {\Gamma \vdash a: \langle \ST_\qual , \overline{\ST}_\qual \rangle &
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, x:\ST}{\INT_1}} }}
\end{equation}
with 
\begin{equation}
\jug_1 = \Gamma; \Theta \vdash \type{\ActS_1}{\INT_1 \addelta a:\ST_\qual} \label{eq:srjug1}
\end{equation}
Then, subtree~\eqref{eq:typerequest} is as follows:
\begin{equation}\label{eq:typerequest}
\infer{\judgebis{\env{\Gamma}{\Theta}}{D\{\nopenr{a}{y}.P_{2} \}}{ \type{\ActS'_2}{ \INT'_2\addelta a:\overline{\ST}_\qual }}}
	{\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2}{ \INT'_2\addelta a:\overline{\ST}_\qual}} &  \infer{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{y}.P_{2}}{ \type{\ActS_2}{ \INT_2\addelta a:\overline{\ST}_\qual }}}
	{\Gamma \vdash a: \langle \ST_\qual , \overline{\ST}_\qual \rangle &
\judgebis{\env{\Gamma}{\Theta}}{P_{2}}{\type{\ActS_2, y:\overline{\ST}}{\INT_2}}}
}
 \end{equation}
 with 
 \begin{equation}
 \jug_2 = \Gamma; \Theta \vdash \type{\ActS_2}{\INT_2 \addelta a:\overline{\ST}_\qual} \label{eq:srjug2}
 \end{equation}
By Lemma~\ref{lem:context} 
% ($\Leftarrow$) 
%there exist $\ActS_1, \ActS_2$ such that 
we have that 
$\ActS_1 \subseteq \ActS_1'$ and $\ActS_2 \subseteq \ActS_2'$. We also infer $\INT_1 \intpr \INT_1'$, $\INT_2 \intpr \INT_2'$, and $\INT' \intpr \INT$. 
 Now, using Lemma~\ref{lem:substitution}(\ref{subchavar}) on judgments for $P_1$ and $P_2$, we obtain:
 \begin{enumerate}[(a)]
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_1\sub{\cha^+}{x}}{ \type{\ActS_1, \cha^+:\ST}{\INT_1}}$.
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}$.
 \end{enumerate}
%By using Lemma \ref{lem:context}($\Rightarrow$)  and typing rules \rulename{t:Par} and \rulename{t:CRes} 
We now describe how to obtain appropriately typed contexts $C^+, D^+$, and $E^{++}$ based on the information inferred up to here
on contexts $C, D$, and $E$.
%We give details for the case of $C^+$; cases for $D^+$ and $E^{++}$ follow analogously. 
We first describe the case of $C^+$.
From \eqref{eq:typeaccept} above we obtained
$\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1 \addelta a:\ST_{\qual}}}$
with $\jug_1$ as in \eqref{eq:srjug1}.
Then, using Lemma~\ref{l:ctxop}(1), we infer
$\judgebis{\bullet_{\jug_3}; \env{\Gamma}{\Theta}}{C^+}{\type{\ActS'_1, \cha^+:\ST}{ \INT'_1}}$
with 
 \begin{equation}
 \jug_3 =  \Gamma; \Theta \vdash \type{\ActS_1, \cha^+:\ST}{\INT_1} \label{eq:srjug3}
 \end{equation}
We may now reconstruct the derivation given in \eqref{eq:typeaccept}:
%$$R \triangleq {{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }},$$
\begin{equation}\label{eq:typeacceptsub}
\infer{\judgebis{\env{\Gamma}{\Theta}}{C^{+}\{P_{1}\sub{\cha^+}{x}\}}{\type{\ActS_1', \cha^+:\ST}{ \INT_1' }}}		  
    { \judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{C^+}{\type{\ActS'_1, \cha^+:\ST\,}{ \INT'_1}} &  
    	\judgebis{\env{\Gamma}{ \Theta}}{P_{1}\sub{\cha^+}{x}}{ \type{\ActS_1, \cha^+:\ST}{\INT_1}}}
\end{equation}
For $D^+$, we proceed analogously from \eqref{eq:typerequest} and infer:
\begin{equation}\label{eq:typerequestsub}
 \infer{\judgebis{\env{\Gamma}{\Theta}}{D^{+}\{P_{2}\sub{\cha^-}{y}\}}{\type{\ActS'_2,\cha^- :\overline{\ST } }{\INT'_2}}}
	{\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D^+}{\type{\ActS'_2, \cha^-:\overline{\ST}}{ \INT'_2}} & \judgebis{\env{\Gamma}{ \Theta}}{P_{2}\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}}
\end{equation}
with 
 \begin{equation}
 \jug_4 =  \Gamma; \Theta \vdash \type{\ActS_2, \cha^-:\overline{\ST}}{\INT_2} \label{eq:srjug4}
 \end{equation}
To infer the type of $E^{++}$ we proceed as before using twice Lemma~\ref{l:ctxop}(1), combined with~\eqref{eq:srjug0}.
We may finally derive the type for the result of the reduction: using rules \rulename{t:Par}, \rulename{t:CRes}, and \rulename{t:Fill} we obtain:
$$
\infer
{\judgebis{\env{\Gamma}{\Theta}}{E^{++}_{} \big\{\restr{\cha}{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\}} \big\} }{\type{\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT''}}}
{(\ref{eq:last})   &
	\infer{\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\}}}{\type{\ActS', [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT_1' \addelta \INT_2'}}}
{\infer{\judgebis{\env{\Gamma}{\Theta}}{{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }}{\type{\ActS', \cha^+:\ST, \cha^-:\overline{\ST} }{ \INT_1' \addelta \INT_2'}}}{
(\ref{eq:typeacceptsub})
%
&
%
	(\ref{eq:typerequestsub})
}
}}
$$
with 
 \begin{equation}\label{eq:last}
\judgebis{\bullet_{\jug_5} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]}{ \INT'' }}
 \end{equation}
and 
$$
 \jug_5 =  \Gamma; \Theta \vdash \type{\ActS', \cha^+:\ST, \cha^-:\overline{\ST} }{ \INT_1' \addelta \INT_2'}
$$

Notice that by Lemma \ref{lem:context}, we have $\INT'' \intpr \INT_1' \cup \INT_2'$.
Also, observe that by assumption $\ActS$ is balanced; therefore, 
by Def.~\ref{d:balanced}
the resulting typing $\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]$ is balanced too.
This concludes this case. 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\paragraph{\bf Case \rulename{r:ROpen}} From Table~\ref{tab:semantics} we have: 
\begin{multline*}
          E\big\{C\{\repopen{a}{x}.P_1\}  \para  D\{\nopenr{a}{y}.P_2\} \big\}  \pired  \\
E^{++}_{}\big\{\restr{\cha}{\big({C^{+}_{}\{P_1\sub{\cha^+}{x}  \para \repopen{a}{x}.P_1 \}  \para  D^{+}_{}\{P_2\sub{\cha^-}{y}\} }\big)}\big\}  
         \end{multline*}

\noindent By assumption $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\repopen{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}\big\} }{\type{\ActS}{\INT}}$, with balanced $\ActS$.  
Then, by inversion on typing, using rules
%is obtained by the following derivation tree using Lemma \ref{lem:context}($\Leftarrow$) three times and inversion on  rules 
\rulename{t:Fill}, 
\rulename{t:RepAccept}, \rulename{t:Request}, and \rulename{t:Par}, we infer there exist $\ActS'$, $\INT'$ such that:
$$
\infer
{ \judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\repopen{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}\big\}}{\type{\ActS}{\INT}}}
{ \judgebis{\bullet_{\jug_0} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{ \INT }}  & \infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\repopen{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}}{\type{\ActS'}{\INT'}}}
{
\eqref{eq:bangaccept}
%
&
%
\eqref{eq:bangrequest}
}}
$$
where
$ \INT' = (\INT'_1 \addelta a:\ST_\quau) \addelta (\INT'_2\addelta a:\overline{\ST}_\qual )$
%$\{ a:\ST_\qual \addelta a:\overline{\ST}_\qual \} \subseteq \INT$, 
and
\begin{equation}
\jug_0 = \Gamma; \Theta \vdash \type{\ActS'}{\INT'} \label{eq:srjugro0}
\end{equation}
By Lemma~\ref{lem:context},  
$\ActS' \subseteq \ActS$ and $\INT' \intpr \INT$.
Then, letting $\ActS' = \ActS'_1 \cup \ActS'_2$, 
subtree \eqref{eq:bangaccept} is as follows:
%where (\ref{}) and (\ref{eq:bangrequest}) correspond to the subtrees:
\begin{equation}\label{eq:bangaccept}
	\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\repopen{a}{x}.P_1\}}{\type{\ActS_1'}{ \INT_1'\addelta a:\ST_\quau }}}		  
    { \judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1\addelta a:\ST_\quau}} & 
    	\infer{\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P_1}{\type{\emptyset}{\,\unres(\INT_1)\addelta a:\ST_\quau }}}
  {\Gamma \vdash a: \langle \ST_\quau , \overline{\ST }_\qual \rangle &
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{x:\ST}{\INT_1}} }}
\end{equation}
with 
\begin{equation}
\jug_1 = \Gamma; \Theta \vdash \type{\emptyset}{\,\unres(\INT_1)\addelta a:\ST_\quau} \label{eq:srjugro1}
\end{equation}
Then, subtree \eqref{eq:bangrequest} is as follows:

\begin{equation}\label{eq:bangrequest}
 \infer{\judgebis{\env{\Gamma}{\Theta}}{D\{\nopenr{a}{y}.P_2 \}}{ \type{\ActS'_2}{ \INT'_2\addelta a:\overline{\ST}_{\qual} }}}
	{\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2}{ \INT'_2\addelta a:\overline{\ST}_\qual}}  & \infer{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{y}.P_2}{ \type{\ActS_2}{ \INT_2\addelta a:\overline{\ST}_{\qual} }}}
	{\Gamma \vdash a: \langle \ST_\quau , \overline{\ST}_\qual \rangle &
\judgebis{\env{\Gamma}{\Theta}}{P_2}{\type{\ActS_2, y:\overline{\ST }}{\INT_2}}}
}
\end{equation}
 with 
 \begin{equation}
 \jug_2 = \Gamma; \Theta \vdash \type{\ActS_2}{\INT_2 \addelta a:\overline{\ST}_\qual} \label{eq:srjugro2}
 \end{equation}
\noindent %where\done\todo[B37.]{Fixed, pls check} 
By Lemma~\ref{lem:context} we have  
$\ActS_1 \subseteq \ActS'_1$ and
$\ActS_2 \subseteq \ActS_2'$. Moreover, $\INT_1 \intpr \INT_1'$, $\INT_2 \intpr \INT_2'$ and $\INT' \intpr \INT$.
% where $ \INT' = (\INT'_1 \addelta \inter{a}{\ST}{\infty}) \addelta (\INT'_2\addelta \inter{a}{\overline{\ST}}{1} )$. 
 Now, using Lemma~\ref{lem:substitution}(\ref{subchavar}) on $P_1$ and $P_2$, we have:
 \begin{enumerate}[(a)]
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_1\sub{\cha^+}{x}}{ \type{ \cha^+:\ST}{\INT_1}}$.
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}$.
 \end{enumerate}
 We now describe how to obtain appropriately typed contexts $C^+, D^+$, and $E^{++}$ based on the information inferred up to here
on contexts $C, D$, and $E$. We first describe the case of $C^+$.
From~\eqref{eq:bangaccept} above we obtained
$\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1 \addelta a:\ST_{\quau}}}$
with $\jug_1$ as in \eqref{eq:srjugro1}.
 Then, using Lemma~\ref{l:ctxop}(1), we infer
$\judgebis{\bullet_{\jug_3}; \env{\Gamma}{\Theta}}{C^+}{\type{\ActS'_1, \cha^+:\ST}{ \INT'_1}}$
with 
 \begin{equation}
 \jug_3 =  \Gamma; \Theta \vdash \type{\cha^+:\ST}{\unres(\INT_1)\addelta a:\ST_\quau} \label{eq:srjugro3}
 \end{equation}
We may now reconstruct the derivation given in \eqref{eq:bangaccept}:
\begin{equation}\label{eq:bangacceptsubfin}
\infer{\judgebis{\env{\Gamma}{\Theta}}{C^{+}\{P_{1}\sub{\cha^+}{x}\}}{\type{\ActS_1', \cha^+:\ST}{ \INT_1' \addelta a:\ST_\quau}}}		  
    { \judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{C^+}{\type{\ActS'_1, \cha^+:\ST\,}{ \INT'_1 \addelta a:\ST_\quau}} &  
    	\judgebis{\env{\Gamma}{ \Theta}}{P_{1}\sub{\cha^+}{x}}{ \type{ \cha^+:\ST}{\unres(\INT_1)\addelta a:\ST_\quau}}}
\end{equation}
For $D^+$, we proceed analogously from \eqref{eq:bangrequest} and infer:
\begin{equation}\label{eq:bangrequestsubfin}
 \infer{\judgebis{\env{\Gamma}{\Theta}}{D^{+}\{P_{2}\sub{\cha^-}{y}\}}{\type{\ActS'_2,\cha^- :\overline{\ST } }{\INT'_2}}}
	{\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D^+}{\type{\ActS'_2, \cha^-:\overline{\ST}}{ \INT'_2}} & \judgebis{\env{\Gamma}{ \Theta}}{P_{2}\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}}
\end{equation}
with 
 \begin{equation}
 \jug_4 =  \Gamma; \Theta \vdash \type{\ActS_2, \cha^-:\overline{\ST}}{\INT_2} \label{eq:srjugro4}
 \end{equation}
To infer the type of $E^{++}$ we proceed as before using twice Lemma~\ref{l:ctxop}(1), combined with~\eqref{eq:srjugro0}.
We may finally derive the type for the result of the reduction: using rules \rulename{t:Par}, \rulename{t:CRes}, and \rulename{t:Fill} we obtain:
$$
\infer
{\judgebis{\env{\Gamma}{\Theta}}{E^{++}_{} \big\{\restr{\cha}{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\}} \big\} }{\type{\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT''}}}
{(\ref{eq:banglast})   &
	\infer{\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\}}}{\type{\ActS', [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT_1' \addelta \INT_2'\addelta a:\ST_\quau}}}
{\infer{\judgebis{\env{\Gamma}{\Theta}}{{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }}{\type{\ActS', \cha^+:\ST, \cha^-:\overline{\ST} }{ \INT_1' \addelta \INT_2'\addelta a:\ST_\quau}}}{
\eqref{eq:bangacceptsubfin}
%
&
%
	\eqref{eq:bangrequestsubfin}
}
}}
$$
with 
 \begin{equation}\label{eq:banglast}
\judgebis{\bullet_{\jug_5} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]}{ \INT'' }}
 \end{equation}
and 
$$
 \jug_5 =  \Gamma; \Theta \vdash \type{\ActS', \cha^+:\ST, \cha^-:\overline{\ST} }{ \INT_1' \addelta \INT_2'\addelta a:\ST_\quau}
$$
Notice that by Lemma \ref{lem:context}, we have $\INT'' \intpr \INT_1' \cup \INT_2'\addelta a:\ST_\quau$.
Also, observe that by assumption $\ActS$ is balanced; therefore, 
by Def.~\ref{d:balanced}
the resulting typing $\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]$ is balanced too.
This concludes this case. 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\paragraph{\bf Case \rulename{r:Upd}} From Table~\ref{tab:semantics} we have:
$$E\big\{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{\mathsf{X}}\}\big\} 
\pired   
E_{}\big\{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}\big\}$$
By assumption we have $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{\mathsf{X}}\}\big\}}{ \type{\ActS}{\INT}}$,
with $\ActS$ balanced.
Then, by inversion on typing, using rules
%is obtained by the following derivation tree using Lemma \ref{lem:context} ($\Leftarrow$) and  inversion on rules 
\rulename{t:Fill}, \rulename{t:Par}, \rulename{t:Adapt}, and \rulename{t:Loc} we infer:
\begin{equation}\label{eq:srupd00}
\infer
{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{\mathsf{X}}\}\big\}}{ \type{\ActS}{\INT}}}
{\judgebis{\bullet_{\jug_0} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{ \INT }}  & \infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{\mathsf{X}}\}}{ \type{\ActS'}{\INT'}}}
{
\eqref{eq:srupd0}
&
\eqref{eq:srupd1}
}}
\end{equation}
with
$\jug_0 =  \Gamma; \Theta \vdash \type{\ActS'}{\INT'}$.
By Lemma~\ref{lem:context}, we have
$\ActS' \subseteq \ActS'$ and $\INT' \intpr \INT$.
Moreover, 
letting $\ActS' = \ActS'_1 \cup \ActS'_2$ and $\INT' = \INT'_1 \addelta \INT'_2$, 
subtree \eqref{eq:srupd0} is as follows:
\begin{equation}\label{eq:srupd0}
\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\component{l}{0}{}{P_1}\} }{ \type{\ActS'_1}{\INT'_1}}}
{\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1 }}  & \infer{\judgebis{\env{\Gamma}{\Theta}}{\compo{l}{0}{P_1}}{ \type{\emptyset}{\INT''_1}}}
{ \INT''_1 \intpr \INT^*_1 & \Theta \vdash l:\INT^*_1
  & \judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\emptyset}{\INT''_1} }   }}
\end{equation}
with
$\jug_1 =  \Gamma; \Theta \vdash \type{\emptyset}{\INT''_1}$,
and $\INT''_1 \intpr \INT'_1$ (by Lemma~\ref{lem:context}).
Subtree \eqref{eq:srupd1} is as follows:
\begin{equation}\label{eq:srupd1}
\infer{\judgebis{\env{\Gamma}{\Theta}}{D\{\adapt{l}{P_2}{\mathsf{X}}\}}{ \type{\ActS'_2}{\INT'_2}}}{
\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2}{ \INT'_2 }} & 
\infer{\judgebis{\env{\Gamma}{\Theta}}{ \adapt{l}{P_2}{\mathsf{X}}}{ \type{\emptyset}{\emptyset}}}
{\Theta \vdash l:\INT^*_1  &  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT^*_1}}}{P_2}{\type{\emptyset}{ \INT_3 }}}}
\end{equation}
with
$\jug_2 =  \Gamma; \Theta \vdash \type{\emptyset}{\emptyset}$.
%By Lemma \ref{lem:context} ($\Leftarrow$) we have $\ActS_1 \cup \ActS_2 \subseteq \ActS$, $\INT_2 \intpr \INT_2'$, $\INT_4 \intpr \INT_4'$, and $\INT_2' \addelta \INT_4' \intpr \INT$. 
By Lemma~\ref{lem:substitution}(\ref{subprovar}) we have  $\judgebis{\env{\Gamma}{\Theta}}{ P_2\sub{P_1}{\mathsf{X}}}{\type{\emptyset}{\INT'_3}}$,
for some $\INT'_3$ such that $\INT'_3 \intpr \INT_3$.
We now reconstruct the derivation in \eqref{eq:srupd00}, using rules
\rulename{t:Par}, \rulename{t:Fill} and Lemma~\ref{l:ctxop}(3). Let
%, thus process $E_{}\big\{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}\big\}$ can be typed by means of Lemma~\ref{lem:context} ($\Rightarrow$) and rule \rulename{t:Par}:
\begin{equation}\label{eq:finupd}
\infer
{\judgebis{\env{\Gamma}{\Theta}}{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}}{ \type{\ActS'_1 \cup \ActS'_2}{\INT''_3 \addelta \INT_2'}}}
{\infer{\judgebis{\env{\Gamma}{\Theta}}{ C\{P_2\sub{P_1}{\mathsf{X}}\} }{\type{\ActS'_1}{\INT''_3}}}{
\judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_1'}{ \INT_3'' }} &
\judgebis{\env{\Gamma}{\Theta}}{ P_2\sub{P_1}{\mathsf{X}}}{\type{\emptyset}{\INT'_3}}}
&
\infer{\judgebis{\env{\Gamma}{\Theta}}{D\{\nil\}}{ \type{\ActS'_2}{\INT'_2}}}{
\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_2'}{ \INT_2' }}
&\judgebis{\env{\Gamma}{\Theta}}{\nil}{ \type{\emptyset}{\emptyset}}}
}
\end{equation}
and
$$
\infer{\judgebis{\env{\Gamma}{\Theta}}{E_{}\big\{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}\big\}}{ \type{\ActS}{\INT'}}}
{\judgebis{\bullet_{\jug_5} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{\INT'}}
&(\ref{eq:finupd})}
$$
with
$$
\begin{array}{c}
\jug_5 =  \Gamma; \Theta \vdash \type{\ActS'_1 \cup \ActS'_2}{\INT''_3 \addelta \INT'_2}
 \end{array}
$$
where by Lemma \ref{lem:context} %($\Rightarrow$) 
we know $\INT_3'' \intpr \INT'_3$ and $\INT_3'' \addelta \INT_2' \intpr \INT'$.
This concludes the analysis for this case.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\paragraph{\bf Case \rulename{r:I/O}} From Table~\ref{tab:semantics} we have:
$$E\big\{C\{\outC{\cha^{\,p}}{\til{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\til{x}}.P_2\}\big\} 
\pired 
E\big\{C\{P_1\} \para  D\{P_2\sub{\til{c}\,}{\til{x}}\}\big\} \quad (\til{e} \downarrow \til{c})$$
By assumption, we have $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\outC{\cha^{\,p}}{\til{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\til{x}}.P_2\}\big\} }{ \type{\ActS}{\INT}}$, with $\ActS$ balanced.
By inversion on typing, using rules 
%we obtain the following derivation that employs Lemma~\ref{lem:context} ($\Leftarrow$) three times and inversion on rules  
\rulename{t:Fill}, \rulename{t:Par}, \rulename{t:In}, and \rulename{t:Out}, we infer:
%$$
%R \triangleq C\{\outC{\cha^{\,p}}{\til{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\til{x}}.P_2\}
%$$
$$
\infer{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\outC{\cha^{\,p}}{\til{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\til{x}}.P_2\}\big\} }{ \type{\ActS}{\INT}}}
{\judgebis{\bullet_{\jug_0} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{\INT}} & \infer
{
\judgebis{\env{\Gamma}{\Theta}}{C\{\outC{\cha^{\,p}}{\til{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\til{x}}.P_2\}} {\type{\ActS'}{ \INT_1' \addelta \INT_2'}}}
{ \eqref{eq:out}
&
\eqref{eq:in}
}}
$$
where:
\begin{eqnarray}
\ActS' & = & \ActS_1' \cup \ActS_2', \cha^p:!(\til{\capab}).{\ST}, \cha^{\overline{p}}:?(\til{\capab}).\overline{\ST} \\
\INT & = & \INT_1' \addelta \INT_2' \\
\jug_0 & = &   \Gamma; \Theta \vdash \type{\ActS'}{\INT'_1 \addelta \INT'_2}
\end{eqnarray}
Moreover, by Lemma~\ref{lem:context}, we infer $\ActS' \subseteq \ActS$ and $\INT'_1 \addelta \INT'_2 \intpr \INT$.
Also, we have that subtree (\ref{eq:out}) 
is as follows:
\begin{equation}\label{eq:out} 
\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\outC{\cha^{p}}{\til{e}}.P_1\} } {\type{\ActS_1',  \cha^p:!(\til{\capab}).{\ST} }{ \INT_1' }}}{
\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_1}{ \INT'_2 }} &   \infer
{\judgebis{\env{\Gamma}{\Theta}}{\outC{\cha^p}{\til{e}}.P_1}{\type{\ActS_1, \cha^p:!(\til{\capab}).{\ST}}{ \INT_1}}}
{\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, \cha^p:{\ST}}{ \INT_1}} & \Gamma \vdash \til{e}:\til{\capab}}}
\end{equation}
with
$$
 \jug_1 =  \Gamma; \Theta \vdash \type{\ActS_1, \cha^p:!(\til{\capab}).{\ST}}{ \INT_1}
$$
Also, subtree (\ref{eq:in}) is as follows:
\begin{equation}\label{eq:in}
 \infer{\judgebis{\env{\Gamma}{\Theta}}{ D\{\inC{\cha^{\overline{p}}}{\til{x}}.P_2\}}{\type{ \ActS_2', \cha^{\overline{p}}:?(\til{\capab}).\overline{\ST}}{ \INT_2'}}}
{\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_1}{ \INT'_2 }} & 
  \infer
{\judgebis{\env{\Gamma}{\Theta}}{\inC{\cha^{\overline{p}}}{\til{x}}.P_1 }{\type{\ActS_2, \cha^{\overline{p}}:?(\til{\capab}).\overline{\ST}}{ \INT_2}}}
{\judgebis{\env{\Gamma, \til{x}:\til{\capab}}{\Theta}}{P_2}{\type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{\INT_2}}}}
\end{equation}
with
$$
 \jug_2 =  \Gamma; \Theta \vdash \type{\ActS_2, \cha^{\overline{p}}:?(\til{\capab}).\overline{\ST}}{ \INT_2}
$$
where Lemma~\ref{lem:context}  ensures $\ActS_1 \subseteq \ActS_1'$, $\ActS_2 \subseteq \ActS_2'$, $\ActS \subseteq \ActS_1' \cup \ActS_2', \cha^p:!(\til{\capab}).{\ST}, \cha^{\overline{p}}:?(\til{\capab}).\overline{\ST} $, $\INT_1 \intpr \INT_1'$, $\INT_2 \intpr \INT_2'$, and $ \INT \intpr \INT_1 \uplus \INT_2$.

Now, by Lemma \ref{lem:substitution}(2)  we know $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\til{c}}{\til{x}}}{\type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{\INT_2}}$ with $\til{e} \downarrow \til{c}$. Moreover by Lemma \ref{l:ctxop}(3) and  rules \rulename{t:Par} and \rulename{t:Fill} we obtain the following type derivations:
\begin{equation}\label{eq:output}
\infer{\judgebis{\env{\Gamma}{ \Theta}}{C\{P_1\}}{\type{\ActS_1', \cha^p:\ST}{\INT_1'}}}
{\judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_1', \cha^p:\ST}{\INT_1'}} 
&
\judgebis{\env{\Gamma}{ \Theta}}{P_1}{\type{\ActS_1, \cha^p:\ST}{\INT_1}}}
\end{equation}
\begin{equation}\label{eq:input}
 \infer{\judgebis{\env{\Gamma}{\Theta}}{D\{P_2\sub{\til{c}\,}{\til{x}}\}}{\type{\ActS_2', \cha^{\overline{p}}:\overline{\ST}}{ \INT_2'}}}{
\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_2', \cha^{\overline{p}}:\overline{\ST}}{ \INT_2'}} 
& \judgebis{\env{\Gamma}{\Theta}}{P_2\sub{\til{c}\,}{\til{x}}}{\type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{ \INT_2}} }
\end{equation}

 $$
\infer{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{P_1\} \para  D\{P_2\sub{\til{c}\,}{\til{x}}\}\big\} }{ \type{\ActS'}{\INT}}}
{\judgebis{\bullet_{\jug_5} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS'}{\INT}}  
 & \infer
{\judgebis{\env{\Gamma}{\Theta}}{C\{P_1\} \para  D\{P_2\sub{\til{c}\,}{\til{x}}\}}{\type{\ActS_1' \cup \ActS_2', \cha^p:\ST, \cha^{\overline{p}}\overline{\ST} }{ \INT_1' \addelta \INT_2'}}}
 {\eqref{eq:output}   & \eqref{eq:input}}
}
$$ 
with
$$
\begin{array}{c}
 \jug_3 =  \Gamma; \Theta \vdash \type{\ActS_1, \cha^p:\ST}{\INT_1}\\
 \jug_4 =  \Gamma; \Theta \vdash \type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{ \INT_2}\\
 \jug_5 =  \Gamma; \Theta \vdash \type{\ActS_1' \cup \ActS_2', \cha^p:\ST, \cha^{\overline{p}}\overline{\ST} }{ \INT_1' \addelta \INT_2'}
\end{array}
$$

Since by inductive hypothesis  $\ActS_1'$ and $\ActS_2'$ are balanced, we infer that  $\ActS_1' \cup \ActS_2', \cha^p:\ST, \cha^{\overline{p}}:\overline{\ST}$ is balanced as well; this concludes the proof for this case.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\paragraph{\bf Case \rulename{r:Pass}} From Table~\ref{tab:semantics} we have:
$$E\big\{C\{\throw{\cha^{\,p}}{\cha_1^{\,q}}.P_1\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.P_2\}\big\}\pired E\big\{C^{-}\{P_1\} \para  D^{+}\{P_2\sub{\cha_1^{\,q}}{x}\}\big\}$$

By assumption we have  $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\throw{\cha^{\,p}}{\cha_1^{\,q}}.P_1\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.P_2\}\big\}}{ \type{\ActS}{\INT}}$, with $\ActS$ balanced. 
By typing inversion on rules 
%Using   Lemma \ref{lem:context} ($\Leftarrow$) and inversion on rules 
\rulename{t:Fill},
\rulename{t:Par}, \rulename{t:Cat}, and \rulename{t:Thr} we infer:
$$
\infer
	{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\throw{\cha^{\,p}}{\cha_1^{\,q}}.P_1\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.P_2\}\big\}}{ \type{\ActS}{\INT}}}
{\judgebis{\bullet_{\jug_0} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{\INT}} & \infer
	{\judgebis{\env{\Gamma}{\Theta}}{C\{\throw{\cha^{p}}{\cha_1^{q}}.P_1\} \para  D\{\catch{\cha^{\overline{p}}}{x}.P_2\}}{ \type{\ActS'}{\INT'}}}
	{
	\eqref{eq:throw}
	&
	\eqref{eq:catch}
	}}
$$
 with: 
 \begin{eqnarray}
 \ActS & = & \ActS_1, \cha^p:!(\ST).\overline{\STT}, \cha_1^{q}:\ST, \ActS_2, \cha^{\overline{p}}:?(\ST).\STT \\
 \ActS' & = & \ActS'_1, \cha^p:!(\ST).\overline{\STT}, \cha_1^{q}:\ST, \ActS'_2, , \cha^{\overline{p}}:?(\ST).\STT \\
 \jug_0 & = &  \Gamma; \Theta \vdash \type{\ActS'}{\INT'} \label{eq:srjugps2}
 \end{eqnarray}
 and, by Lemma~\ref{lem:context}, we infer $\ActS'_1 \subseteq \ActS_1$, $\ActS'_2 \subseteq \ActS_2$, and $\INT' \intpr \INT$.
 Moreover, \eqref{eq:throw}  corresponds to the subtree:
\begin{equation}\label{eq:throw}
 \infer
		{\judgebis{\env{\Gamma}{\Theta}}{C\{\throw{\cha^{p}}{\cha_1^{q}}.P_1\} }{ \type{\ActS'_1, \cha^p:!(\ST).\overline{\STT}, \cha_1^{q}:\ST}{ \INT'_1}}}
		{\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1, \cha^p:!(\ST).\overline{\STT},\, \cha_1^{q}:\ST}{ \INT'_1 }}  & \infer
{\judgebis{\env{\Gamma}{\Theta}}{\throw{\cha^p}{\cha_1^{q}}.P_1}{\type{\ActS''_1,\, \cha^p:!(\ST).\overline{\STT},\, \cha_1^{q}:\ST}{ \INT''_1}}}
{\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS''_1, \cha^p:\overline{\STT}}{ \INT''_1}} 
		}}
\end{equation}
with $\ActS''_1 \subseteq \ActS'_1$ and $\INT''_1 \intpr \INT'_1$ (by Lemma~\ref{lem:context}) and
 \begin{eqnarray}
 \jug_1 & = &  \Gamma; \Theta \vdash \type{\ActS''_1,\, \cha^p:!(\ST).\overline{\STT},\, \cha_1^{q}:\ST}{\INT''_1} \label{eq:srjugps3}
 \end{eqnarray}
while \eqref{eq:catch}   corresponds to the subtree:
\begin{equation}\label{eq:catch}
 \infer
		{\judgebis{\env{\Gamma}{\Theta}}{ D\{\catch{\cha^{\overline{p}}}{x}.P_2\}}{ \type{\ActS'_2, \cha^{\overline{p}}:?(\ST).\STT}{ \INT'_2}}}
		{\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2, \cha^{\overline{p}}:?(\ST).\STT}{ \INT'_2 }} & \infer
{\judgebis{\env{\Gamma}{\Theta}}{\catch{\cha^{\overline{p}}}{x}.P_2 }{\type{\ActS''_2, \cha^{\overline{p}}:?(\ST).\STT}{\INT''_2}}}
{\judgebis{\env{\Gamma}{\Theta}}{P_2}{\type{\ActS''_2, \cha^{\overline{p}}:\STT, x:\ST}{\INT''_2}}}	
}
\end{equation}
with $\ActS''_2 \subseteq \ActS'_2$ and $\INT''_2 \intpr \INT'_2$ (by Lemma~\ref{lem:context}) and
 \begin{eqnarray}
 \jug_2 & = &  \Gamma; \Theta \vdash \type{\ActS''_2, \cha^{\overline{p}}:?(\ST).\STT}{\INT''_2} \label{eq:srjugps4}
 \end{eqnarray}
%
%and where by Lemma \ref{lem:context} ($\Leftarrow$) ensures $\ActS_1 \subseteq \ActS_1'$, $\ActS_2 \subseteq \ActS_2'$, $\ActS' \subseteq \ActS$ and $\ActS' = \ActS'_1 \cup \ActS'_2,  \cha^p:!(\ST).\overline{\STT}, \cha_1^q:\ST, \cha^{\overline{p}}:?(\ST).\STT$. Moreover we have $\INT_1 \intpr \INT_1'$, $\INT_2 \intpr \INT_2'$, $\INT' \intpr \INT$ and $\INT' = \INT'_1 \addelta \INT'_2$. Notice that as $\ActS$ is balanced, in $\ActS$ there is a $\cha_1^{\overline{q}}:\overline{\ST}$.

We now describe how to obtain appropriately typed contexts $C^-$ and $D^+$, 
based on the information already inferred  on contexts $C$ and $D$.
We first consider the case of $C^-$. From \eqref{eq:throw}, we obtained 
$$
\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1, \cha^p:!(\ST).\overline{\STT},\, \cha_1^{q}:\ST}{ \INT'_1 }}
$$
with $\jug_1$ as in \eqref{eq:srjugps3}. Then, using Lemma~\ref{l:ctxop}(2), we infer 
$$
\judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{C^-}{\type{\ActS'_1, \cha^p:\overline{\STT}}{ \INT'_1 }}
$$
where 
 \begin{eqnarray}
 \jug_3 & = &  \Gamma; \Theta \vdash \type{\ActS''_1,\, \cha^p: \overline{\STT} }{\INT''_1}  \label{eq:srjugps5}
 \end{eqnarray}
We may now reconstruct the derivation in~\eqref{eq:throw}, as follows:
\begin{equation}\label{eq:passd}
\infer
		{\judgebis{\env{\Gamma}{\Theta}}{C^{-}\{P_1\} }{ \type{\ActS'_1, \cha^p:\overline{\STT}}{ \INT'_1}}}
		{\judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{C^-}{\type{\ActS'_1, \cha^p:\overline{\STT}}{ \INT'_1 }} &\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS''_1, \cha^p:\overline{\STT}}{ \INT''_1}} 
		}
\end{equation}
We now consider the case of $D^+$.
By applying Lemma \ref{lem:substitution} \eqref{subchavar}
on the premise concerning $P_2$ in \eqref{eq:catch}, we obtain
$$\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha_1^q}{x}}{\type{\ActS''_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{ \INT''_2}}$$ 
From \eqref{eq:catch} we obtained
$$
\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2, \cha^{\overline{p}}:?(\ST).\STT}{ \INT'_2 }}
$$
with $\jug_2$ as in \eqref{eq:srjugps4}. Then, using Lemma~\ref{l:ctxop}(1), we infer 
$$
\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D^+}{\type{\ActS'_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{ \INT'_2 }}
$$
where
 \begin{eqnarray}
 \jug_4 & = &  \Gamma; \Theta \vdash \type{\ActS''_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{\INT''_2} \label{eq:srjugps6}
 \end{eqnarray}
We can reconstruct the derivation depicted by \eqref{eq:catch}:
%thus obtaining the following typing tree where we have used Lemma \ref{lem:context} ($\Rightarrow$) and rule \rulename{t:Par}, we also use the following subtree:
\begin{equation}\label{eq:pass}
 \infer
		{\judgebis{\env{\Gamma}{\Theta}}{ D^{+}\{P_2\sub{\cha_1^{q}}{x}\}}{ \type{\ActS'_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{ \INT'_2}}}
		{\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D^+}{\type{\ActS'_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{ \INT'_2 }} & \judgebis{\env{\Gamma}{\Theta}}{P_2\sub{\cha_1^{q}}{x}}{\type{\ActS''_2, \cha^+:\STT, \cha_1^q:\ST}{\INT''_2}}	
}
\end{equation}
Combining 
\eqref{eq:passd} and \eqref{eq:pass}, 
we may finally derive the type for the result of the reduction. Using rules \rulename{T:Par}  and \rulename{T:Fill} we obtain:
$$
\infer
	{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C^{-}\{P_1\} \para  D^{+}\{P_2\sub{\cha_1^{q}}{x}\}\big\}}{ \type{\ActS^*}{\INT}}}
{\judgebis{\bullet_{\jug_5} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS^*}{\INT}}
 & \infer
	{\judgebis{\env{\Gamma}{\Theta}}{C^{-}\{P_1\} \para  D^{+}\{P_2\sub{\cha_1^{q}}{x}\}}{ \type{\ActS'_1 \cup \ActS'_2, \cha^p:\overline{\STT}, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{\INT'}}}
	{\eqref{eq:passd} & \eqref{eq:pass}
	}}
$$
with
$$
\jug_5 =  \Gamma; \Theta \vdash \type{\ActS'_1 \cup \ActS'_2, \cha^p:\overline{\STT}, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{\INT'}
$$
Since by assumption $\ActS$ is balanced, we have that 
by construction $\ActS^*$ is balanced as well. It is worth observing how contexts $C^{-}$ and $D^{+}$ correctly implement the fact that the number of active sessions is changed after delegating session $\kappa_1^{q}$ to process $P_2$.
 This concludes the proof for this case.


% 
\paragraph{\bf Cases \rulename{r:IfTr} and \rulename{r:IfFa}} Follows by an ease induction on the derivation tree.

% 
\paragraph{\bf Case \rulename{r:Close}} These follow by the same reasoning as in  \rulename{r:Open} case.
% 
\paragraph{\bf Case \rulename{r:Branch}} This case is similar to  previous \rulename{r:I/O} case. 
% 
\paragraph{\bf Case \rulename{r:Str}} Follows from Theorem~\ref{th:congr} (Subject Congruence).
% 
\paragraph{\bf Case \rulename{r:Par}} Follows by induction and by applying rule $\rulename{t:Par}$.
%
\paragraph{\bf Case \rulename{r:Res}} Follows by induction and by the fact that  $\ActS$ is balanced. Indeed, by hypothesis and by inversion on rule \rulename{t:CRes} all the occurences of bracketed assignements ($[\cha^p:\ST]$) are necessarily balanced thus making it possible to apply the inductive hypothesis to the premise of the rule and concluding the analysis of this case and the proof of the theorem.
% \end{description}
\end{proof}



\section{Additional Material for \S\,\ref{sec:disc}\label{ap:addmat}}
\begin{table}[t]
{
$$
\begin{array}{ll}
 \rulename{r:LPar} & \text{if } P \pired P' ~~\text{then} ~~ P \para Q \pired P' \para Q  \vspace{2mm}
\\
 \rulename{r:LRes} &
\text{if } P \pired P' ~~\text{then} ~~ \restr{\cha}{P} \pired \restr{\cha}{P'} %\vspace{2mm} \\
\vspace{2.0mm} \\
 \rulename{r:LStr} &
\text{if } P \equiv P',\, P' \pired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \pired Q \vspace{2mm}
\\
  \rulename{r:LLoc} &
 \text{if } P \pired P'~~\text{then}~~ \scomponent{l}{P} \pired \scomponent{l}{P'} \vspace{2mm}
 \\ 
 \rulename{r:LOpen} & 
C\{\nopena{a}{x}.P\} \para  D\{\nopenr{a}{y}.Q\} \pired  \\
& 
\hfill \restr{\cha}{\big({C\{P\sub{\cha^+}{x}\}  \para  D\{Q\sub{\cha^-}{y}\} }\big) } \vspace{2.0mm} \\
\rulename{r:LROpen} & 
C\{\repopen{a}{x}.P\}  \para  D\{\nopenr{a}{y}.Q\}   \pired  \\
& 
\hfill \restr{\cha}{\big({C\{P\sub{\cha^+}{x}  \para \repopen{a}{x}.P \}  \para  D\{Q\sub{\cha^-}{y}\} }\big)} 
 \vspace{2.0mm}\\
\rulename{r:LUpd} & 
C\{\component{l}{}{}{P}\} \para  D\{\adapt{l}{Q}{X}\} 
\pired   %\\
%& \hfill 
C\{Q\sub{P}{\mathsf{X}}\}  \para  D\{\nil\} \vspace{2mm} \\

\rulename{r:LI/O} &
C\{\outC{\cha^{\,p}}{\widetilde{e}}.P\} \para  D\{\inC{\cha^{\,\overline{p}}}{\widetilde{x}}.Q\}
\pired %\\
%& \hfill 
C\{P\} \para  D\{Q\sub{\widetilde{c}\,}{\widetilde{x}}\} \quad (\widetilde{e} \downarrow \widetilde{c}) \vspace{2mm}
\\
\rulename{r:LPass} &
C\{\throw{\cha^{\,p}}{\cha'^{\,q}}.P\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.Q\}\pired  C\{P\} \para  D\{Q\sub{\cha'^{\,q}}{x}\} %\\
%& \hfill E\big\{C^{-}\{P\} \para  D^{+}\{Q\sub{\cha'^{\,q}}{x}\}\big\} 
\vspace{2mm}
\\
\rulename{r:LSel} &
C\{\branch{\cha^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m}\} \para  D\{\select{\cha^{\,\overline{p}}}{n_j};Q\} 
\pired \\
& 
\hfill C\{P_j\}\para  D\{Q\}  \quad (1 \leq j \leq m)  \vspace{2mm}
\\
\rulename{r:LClose} &
C\{\close{\cha^{\,p}}.P\} \para  D\{\close{\cha^{\,\overline{p}}}.Q\} \pired %\\
%& \hfill 
C\{P\} \para  D\{Q\} \vspace{ 2mm}
\\
\rulename{r:LIfTr} &
\ifte{e}{P}{Q} \pired P  \quad (e \downarrow \mathtt{true})  \vspace{2mm}
\\
 \rulename{r:LIfFa} &
\ifte{e}{P}{Q} \pired Q  \quad (e \downarrow \mathtt{false}) \vspace{2mm}
\end{array}
$$
}
\caption{Reduction semantics without annotations. } \label{tab:semanticsnoannot}
\end{table}




 \begin{table}[t]
 $$
 \begin{array}{lc}
 \rulename{r:ParU} &
 \infer{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{ \type{\ActS_1 \cup \ActS_2}{\INT_1 \cup \INT_2 }} \pired \judgebis{\env{\Gamma}{\Theta}}{P' \para Q}{ \type{\ActS_1' \cup \ActS_2}{\INT_1' \uplus \INT_2' }}}{ \judgebis{\env{\Gamma}{\Theta}}{P }{ \type{\ActS_1}{\INT_1 }} \pired \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS_1'}{\INT_1' }}}
  \\ \\ 
 \rulename{r:ResU} &
 \infer{
 \begin{array}{c}
 \judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{P}}{ \type{[\cha^+:\alpha], [\cha^-:\overline{\alpha}],\ActS}{\INT }} \pired \\
 \judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{P'} }{ \type{[\cha^+:\alpha'],[ \cha^-:\overline{\alpha'}],\ActS' }{\INT'  }}
 \end{array}
 }
 {\judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\cha^+:\alpha, \cha^-:\overline{\alpha},\ActS}{\INT }} \pired \judgebis{\env{\Gamma}{\Theta}}{P' }{\type{\cha^+:\alpha', \cha^-:\overline{\alpha'},\ActS'}{\INT' }}}
 \\ \\
 \rulename{r:StrU} &
 \infer{\judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS}{\INT }} \pired \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS'}{\INT'}}}{P \equiv Q \quad \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS}{\INT }} \pired \judgebis{\env{\Gamma}{\Theta}}{Q'}{ \type{\ActS'}{\INT'}} \quad  P' \equiv Q'}
  \\ \\
  \rulename{r:LocU} &
 \infer{\judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P}}{ \type{\ActS}{\INT }} \pired \judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P'}}{ \type{\ActS'}{\INT'}}}{\judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS}{\INT }} \pired \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS'}{\INT'}} }
 \\ \\
 \rulename{r:UpdU} &
\infer{
\begin{array}{c}
\judgebis{\env{\Gamma}{\Theta}}{C\{\scomponent{l}{P}\} \para  D\{\adapt{l}{Q}{X}\}}{\type{\ActS}{\INT}}
\\
\pired \\ 
 \judgebis{\env{\Gamma}{\Theta}}{C\{\rho(Q)\sub{P}{\mathsf{X}}\}  \para  D\{\nil\}}{\type{\ActS}{(\INT \setminus \INT_1) \uplus \INT_2}}
\end{array}
}
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{\INT_1}} \quad \judgebis{\env{\Gamma}{\Theta, \mathsf{X}:\ActS_1,\INT_1}}{Q}{\type{\ActS_2}{\INT_2}} \quad \ActS_1 = \rho(\ActS_2)}
 \\ \\
  \rulename{r:IfTrU} &
 \judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{ \type{\ActS}{\INT}}  \pired \judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS}{\INT}} \quad (e \downarrow \mathtt{true}) \vspace{0.2cm}  
 \\ 
  \rulename{r:IfFaU} &
 \judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{ \type{\ActS}{\INT}}  \pired \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS}{\INT}} \quad (e \downarrow \mathtt{false})  
 \end{array}
 $$
 \caption{Typed reduction semantics. (I)}\label{tab:1typedsemantics} 
\end{table}

 
 \begin{table}[t]
  $$
  \begin{array}{l}
 \rulename{r:OpenU} \\ 
 \judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{a}{x}.P\} \para D\{\nopenr{a}{y}.Q\}}{ \type{\ActS}{\INT, a:\alpha_{\qual}, a:\overline{\alpha}_{\qual} }}  \pired \\
  \hfill \judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{C\{P\sub{\cha^+}{x}\} \para D\{Q\sub{\cha^-}{y}}\}}{ \type{\ActS,[\cha^+:\alpha],[\cha^-:\overline{\alpha}]}{\INT}}
 \\ \\ 
 \rulename{r:ROpenU} \\ 
 \judgebis{\env{\Gamma}{\Theta}}{C\{\repopen{a}{x}.P\} \para D\{\nopenr{a}{y}.Q\}}{ \type{\ActS}{\INT, a:\alpha_{\quau}, a:\overline{\alpha}_{\qual} }}  \pired
  \\   \hfill \judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{C\{P\sub{\cha^+}{x} \para \repopen{a}{x}.P\}\para D\{Q\sub{\cha^-}{y}}\}}{ \type{\ActS,[\cha^+:\alpha],[\cha^-:\overline{\alpha}]}{\INT,a:\alpha_{\quau}}}
 \\ \\
  \rulename{r:I/OU} \\
 \judgebis{\env{\Gamma}{\Theta}}{C\{\outC{\cha^{\,p}}{\widetilde{e}}.P\} \para D\{\inC{\cha^{\,\overline{p}}}{\widetilde{x}}.Q\}}{ \type{\ActS,\cha^{p}:!(\tilde{\capab}).\ST, \cha^{\overline{p}}:?(\tilde{\capab}).\overline{\ST}}{\INT}}  \pired \\
  \hfill \judgebis{\env{\Gamma}{\Theta}}{C\{P\} \para D\{Q \sub{\widetilde{c}\,}{\widetilde{x}}\}}{ \type{\ActS,\cha^{p}:\ST, \cha^{\overline{p}}:\overline{\ST}}{\INT}}
 \\ \\
  \rulename{r:PassU} \\
 \judgebis{\env{\Gamma}{\Theta}}{C\{\throw{\cha^{\,p}}{\cha'^{\,q}}.P\} \para D\{\catch{\cha^{\,\overline{p}}}{x}.Q\}}{ \type{\ActS,\cha^{p}:!(\ST).\STT,\cha'^{q}:\ST, \cha^{\overline{p}}:?(\ST).\overline{\STT}}{\INT}}  \pired \\
  \hfill \judgebis{\env{\Gamma}{\Theta}}{C\{P\} \para D\{Q\sub{\cha'^{\,q}}{x}\}}{ \type{\ActS,\cha^{p}:\STT, \cha^{\overline{p}}:\overline{\STT}, \cha'^{q}:\ST}{\INT}}
 \\ \\
  \rulename{r:SelU} \\
 \judgebis{\env{\Gamma}{\Theta}}{C\{\branch{\cha^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m}\} \para  D\{\select{\cha^{\,\overline{p}}}{n_j};Q\}}{
 \\  \type{\ActS,\cha^{p}:\&\{n_1{:}\ST_1, \ldots, n_k{:}\ST_m \}, \cha^{\overline{p}}:\oplus\{n_1:\overline{\ST_1}, \ldots,  n_m:\overline{\ST_m} \} }{\INT}}  \pired \\
  \hfill \judgebis{\env{\Gamma}{\Theta}}{C\{P_j\} \para D\{Q\} }{ \type{\ActS,\cha^{p}:\ST_j, \cha^{\overline{p}}:\overline{\ST_j}}{\INT}}
 \\ \\
  \rulename{r:CloseU} \\
 \judgebis{\env{\Gamma}{\Theta}}{C\{\close{\cha^{\,p}}.P\} \para D\{\close{\cha^{\,\overline{p}}}.Q\}}{ \type{\ActS,\cha^{p}:\epsilon, \cha^{\overline{p}}:\epsilon}{\INT}}  \pired \\
  \hfill \judgebis{\env{\Gamma}{\Theta}}{C\{P\} \para D\{Q\} }{ \type{\ActS}{\INT}}
 \end{array}
 $$
 \caption{Typed reduction semantics. (II)}\label{tab:typedsemantics} 
 \end{table}




% 
% \begin{table}[t!]
% $$
% \begin{array}{c}
% \inferrule*[left=\rulename{l:Accept}]{\INT = \INT' \uplus a:\alpha_{\qual}}{
% \judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P}{ \type{\ActS}{\INT}} \xrightarrow{\open{a}} \judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS,x:\alpha}{\INT}}}
% \\ \\ 
% \inferrule*[left=\rulename{l:Request}]{\INT = \INT' \uplus  a:\overline{\alpha}_{\qual} }
% {\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{y}.Q}{ \type{\ActS}{\INT  }}  
% \xrightarrow{\overline{\open{a}}}  
% \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS,y:\overline{\alpha}}{\INT'}}}
% \\ \\
% \inferrule[\rulename{l:RAccept}]{\INT = \INT'  \uplus a:\alpha_{\quau} }{
% \judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P}{ \type{\ActS}{\INT }} \xrightarrow{\open{a}} 
% %\\ \hfill
%  \judgebis{\env{\Gamma}{\Theta}}{P \para \repopen{a}{x}.P}{ \type{\ActS,x:\alpha}{\INT}}}
% \\ \\
% \inferrule*[left=\rulename{l:Out}]{\widetilde{e} \downarrow \widetilde{c} \qquad \ActS = \ActS_1,\cha^{p}:!(\tilde{\capab}).\ST \qquad \ActS' = \ActS_1,\cha^{p}: \ST}
% {{\judgebis{\env{\Gamma}{\Theta}}{\outC{\cha^{\,p}}{\widetilde{e}}.P}{ \type{\ActS}{\INT}}  \xrightarrow{\cha^{\,p}(\widetilde{c})}  \judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS'}{\INT}}}}
% \\ \\
% \inferrule*[left=\rulename{l:In}]{\ActS = \ActS_1, \cha^{\overline{p}}:?(\tilde{\capab}).\overline{\ST} \qquad \ActS' = \ActS_1, \cha^{\overline{p}}:\overline{\ST}}{
% \judgebis{\env{\Gamma}{\Theta}}{\inC{\cha^{\,\overline{p}}}{\widetilde{x}}.Q}{ \type{\ActS}{\INT}}  \xrightarrow{\cha^{\,\overline{p}}(\widetilde{c})} 
%  \judgebis{\env{\Gamma}{\Theta}}{Q \sub{\widetilde{c}\,}{\widetilde{x}}}{ \type{\ActS'}{\INT}}}
% \\ \\
% \inferrule*[left=\rulename{l:Throw}]{\ActS = \ActS_1,\cha^{p}:!(\ST).\STT,\cha'^{q}:\ST \qquad \ActS' = \ActS_1,\cha^{p}:\STT}{
% \judgebis{\env{\Gamma}{\Theta}}{\throw{\cha^{\,p}}{\cha'^{\,q}}.P}{ \type{\ActS}{\INT}}  \xrightarrow{\cha^{\,p}(\cha'^{\,q})} %\\ \hfill 
%  \judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS'}{\INT}}}
% \\ \\
% \inferrule*[left=\rulename{l:Catch}]{\ActS = \ActS_1, \cha^{\overline{p}}:?(\ST).\overline{\STT} \qquad \ActS' = \ActS_1, \cha^{\overline{p}}:\overline{\STT}, \cha'^{q}:\ST}
% {\judgebis{\env{\Gamma}{\Theta}}{\catch{\cha^{\,\overline{p}}}{x}.Q}{ \type{\ActS}{\INT}}  \xrightarrow{\cha^{\,\overline{p}}(\cha'^q)} 
% %\\ \hfill 
% \judgebis{\env{\Gamma}{\Theta}}{Q\sub{\cha'^{\,q}}{x}}{ \type{\ActS'}{\INT}}}
% \\ \\
% \inferrule*[left=\rulename{l:Close}]{ } {
% \judgebis{\env{\Gamma}{\Theta}}{\close{\cha^{\,p}}.P\} }{ \type{\ActS,\cha^{p}:\epsilon}{\INT}}  \xrightarrow{\kappa^p(\closeact)} 
%  \judgebis{\env{\Gamma}{\Theta}}{P }{ \type{\ActS}{\INT}}}
%  \\ \\
% \inferrule[\rulename{l:Branch}]{\ActS = \ActS_1,\cha^{p}:\&\{n_1{:}\ST_1, \ldots, n_k{:}\ST_m \} \qquad \ActS' = \ActS_1,\cha^{p}:\ST_j \qquad j \in [1..m]}{
% \judgebis{\env{\Gamma}{\Theta}}{\branch{\cha^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m}}{
% \type{\ActS}{\INT}}  \xrightarrow{\kappa^p(n_j)}  \judgebis{\env{\Gamma}{\Theta}}{P_j }{ \type{\ActS'}{\INT}}}
%  \\ \\
%  \inferrule*[left=\rulename{l:Sel}]{\ActS = \ActS_1, \cha^{\overline{p}}:\oplus\{n_1:\overline{\ST_1}, \ldots,  n_m:\overline{\ST_m} \} \qquad \ActS' = \ActS_1, \cha^{\overline{p}}:\overline{\ST_j}}{
% \judgebis{\env{\Gamma}{\Theta}}{\select{\cha^{\,\overline{p}}}{n_j};Q}{
%  \type{\ActS}{\INT}}  \xrightarrow{\kappa^{\overline{p}}(n_j)} 
%  \hfill \judgebis{\env{\Gamma}{\Theta}}{Q }{ \type{\ActS'}{\INT}}}
% \end{array}
% $$
% \caption{Typed LTS (I)\label{t:typedltsi}}
% \end{table}
% 
% 
% \begin{table}[t!]
% $$
% \begin{array}{c}
%  \inferrule*[left=\rulename{l:Par1}]{ \judgebis{\env{\Gamma}{\Theta}}{P }{ \type{\ActS_P}{\INT_P }} \xrightarrow{\act} \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS_P'}{\INT_P' }} \qquad \mathsf{bc}(\act) \cap \mathsf{fc}(Q) = \emptyset }{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{ \type{\ActS}{\INT }} \xrightarrow{\act} \judgebis{\env{\Gamma}{\Theta}}{P' \para Q}{ \type{\ActS \setminus \ActS_P \cup \ActS_P'}{\INT \setminus \INT_P \uplus \INT_P' }}}
% \\ \\ 
%  \\
% \inferrule[\rulename{l:Open}]
% { 
% %\begin{array}{c}
% \judgebis{\env{\Gamma}{\Theta}}{P }{ \type{\ActS_P}{\INT_P}} \xrightarrow{\open{a}} \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS_P, x:\alpha}{\INT_P'}}\\
% \judgebis{\env{\Gamma}{\Theta}}{Q }{ \type{\ActS_Q}{\INT_Q }} \xrightarrow{\overline{\open{a}}} \judgebis{\env{\Gamma}{\Theta}}{Q'}{ \type{\ActS_Q, y:\overline{\alpha}}{\INT_Q' }}\\
% \ActS= \ActS_P \cup \ActS_Q \qquad \INT=\INT_P \uplus \INT_Q  \qquad \INT'=\INT_P' \uplus \INT_Q'
%  % \end{array}
% }{
% %\begin{array}{c}
% \judgebis{\env{\Gamma}{\Theta}}{P \para Q}{ \type{\ActS}{\INT}} \xrightarrow{\tau}  \judgebis{\env{\Gamma}{\Theta}}{\restr{\kappa}{(P'\sub{\kappa^+}{x} \para Q'\sub{\kappa^-}{y})}}{ \type{\ActS, [\kappa^+:\alpha], [\kappa^-:\overline{\alpha}]}{\INT' }} 
% %\end{array}
% }
%  \\ \\
% %  
% % \rulename{l:ROpen} \\
% % \infer{
% % \begin{array}{c}
% % \judgebis{\env{\Gamma}{\Theta}}{P \para Q}{ \type{\ActS}{\INT\uplus \{a:\alpha_\quau, a:\overline{\alpha}_\qual  \}}} \xrightarrow{\tau} \\ \judgebis{\env{\Gamma}{\Theta}}{\restr{\kappa}{(P'\sub{\kappa^+}{x} \para Q'\sub{\kappa^-}{y})}}{ \type{\ActS, [\kappa^+:\alpha], [\kappa^-:\overline{\alpha}]}{\INT \uplus a:\alpha_\quau }} 
% % \end{array}
% % }
% % { \begin{array}{c}
% % \judgebis{\env{\Gamma}{\Theta}}{P }{ \type{\ActS_P}{\INT_P \uplus a:\alpha_\quau }} \xrightarrow{\open{a}} \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS_P, x:\alpha}{\INT_P\uplus a:\alpha_\quau} }\\
% % \judgebis{\env{\Gamma}{\Theta}}{Q }{ \type{\ActS_Q}{\INT_Q \uplus a:\overline{\alpha}_\qual }} \xrightarrow{\overline{\open{a}}} \judgebis{\env{\Gamma}{\Theta}}{Q'}{ \type{\ActS_Q, y:\overline{\alpha}}{\INT_Q } }\\
% %  \ActS= \ActS_P \cup \ActS_Q \qquad \INT=\INT_P \uplus \INT_Q
% %   \end{array}
% % }
% %  \\ \\
%  
%  \inferrule[\rulename{l:Com}]
%  { %\begin{array}{c}
% \judgebis{\env{\Gamma}{\Theta}}{P }{ \type{\ActS_P}{\INT_P }} \xrightarrow{\restr{\widetilde{\cha}}{\act}} \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS_P'}{\INT_P' }}                                                                                                \\
% \judgebis{\env{\Gamma}{\Theta}}{Q }{ \type{\ActS_P}{\INT_P }} \xrightarrow{\overline{\act}} \judgebis{\env{\Gamma}{\Theta}}{Q'}{ \type{\ActS_Q'}{\INT_Q' } \qquad \widetilde{\cha} \cap \mathsf{fc}(Q) = \emptyset }
%   %\end{array}
% }
% {\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{ \type{\ActS_P \cup \ActS_Q}{\INT_P \uplus \INT_Q }} \xrightarrow{~\tau~} \judgebis{\env{\Gamma}{\Theta}}{\restr{\widetilde{\cha}}{(P' \para Q')}}{ \type{\ActS_P' \cup \ActS_Q'}{\INT_P' \uplus \INT_Q' }}}
% 
% \\ \\
%  \inferrule[\rulename{l:Adapt}] 
% {\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_P}{\INT_P}} \quad \judgebis{\env{\Gamma}{\Theta, \mathsf{X}:\ActS_P,\INT_P}}{Q}{\type{\ActS_Q}{\INT_Q}} \qquad \ActS_P = \ActS_Q[\rho]}{
% \judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P}}{\type{\ActS_P}{\INT_P}} \xrightarrow{\overline{\adapt{l}{Q}{X}}} 
% \judgebis{\env{\Gamma}{\Theta}}{Q\sub{P}{\mathsf{X}}[\rho]\}}{\type{\ActS_Q[\rho]}{ \INT_Q}}
% }
% \\ \\
%  \inferrule[\rulename{l:JAdapt}] 
% {\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} \qquad \judgebis{\env{\Gamma}{\Theta, \mathsf{X}:\ActS',\INT}}{Q}{\type{\ActS_1}{\INT_1}} \quad \rho = \subst{\cha^{p}_1, \ldots, \cha^{p}_m}{x_1, \ldots, x_m} \quad \ActS = \rho(\ActS')}{
% \judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P}}{\type{\ActS_1}{\INT_1}} \xrightarrow{\overline{\adapt{l}{Q}{\mathsf{X}}}} 
% \judgebis{\env{\Gamma}{\Theta}}{\rho(Q)\sub{P}{\mathsf{X}}}{\type{\rho(\ActS_1)}{\INT_1}}
% }
% 
% \\ \\
%  \inferrule[\rulename{l:Update}]{ }{
% \judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{Q}{\mathsf{X}}}{\type{\emptyset}{\emptyset}} \xrightarrow{\adapt{l}{Q}{\mathsf{X}}}  
% \judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}
% \end{array}
% $$
% \caption{Typed LTS (II)\label{t:typedltsii}}
% \end{table}
% 
% 
% \begin{table}
% $$
% \begin{array}{c}
% 
% \inferrule[\rulename{l:NameExtr}]
% {
% \judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS, \cha^p:\alpha}{\INT }} \xrightarrow{\act} \judgebis{\env{\Gamma}{\Theta}}{P' }{\type{\ActS', \cha^p:\alpha'}{\INT' }} 
% \qquad \cha \in \mathsf{fc}(\act)
% }{
% \judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{P}}{ \type{\ActS,[\cha^p:\alpha]}{\INT }} \xrightarrow{\restr{\cha}{\act}} \judgebis{\env{\Gamma}{\Theta}}{P' }{\ActS', \type{[\cha^p:\alpha;] }{\INT'  }}
% }
% \\ \\ 
% 
% 
% 
% \inferrule[\rulename{l:Res}]
% {
% %\begin{array}{c}
% \judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\cha^+:\alpha, \cha^-:\overline{\alpha},\ActS}{\INT }} \xrightarrow{\act} \judgebis{\env{\Gamma}{\Theta}}{P' }{\type{\cha^+:\alpha', \cha^-:\overline{\alpha'},\ActS'}{\INT' }} \qquad
% \cha \notin \mathsf{bc}(\act) \cup \mathsf{fc}(\act)
% %\end{array}
% }
% {
% %\begin{array}{c}
% \judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{P}}{ \type{[\cha^+:\alpha], [\cha^-:\overline{\alpha}],\ActS}{\INT }} \xrightarrow{\act} 
% \judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{P'} }{ \type{[\cha^+:\alpha'],[ \cha^-:\overline{\alpha'}],\ActS' }{\INT'  }}
% %\end{array}
% }
% 
% \\ \\
% \inferrule[\rulename{l:Str}]
% {P \equiv_{\alpha} Q \quad \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS}{\INT }} \xrightarrow{\act} \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS'}{\INT'}} }{\judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS}{\INT }} \xrightarrow{\act} \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS'}{\INT'}}}
%  \\ \\
% \inferrule[ \rulename{l:Loc}]
% {\judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS}{\INT }} \xrightarrow{\act} \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS'}{\INT'}} }{\judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P}}{ \type{\ActS}{\INT }} \xrightarrow{\act} \judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P'}}{ \type{\ActS'}{\INT'}}}
% \\ \\
% \inferrule[ \rulename{l:IfTr}]{(e \downarrow \mathtt{true}) }
% {\judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{ \type{\ActS}{\INT}}  \xrightarrow{~\tau~} \judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS}{\INT}}} 
% \\ 
%  \inferrule[ \rulename{l:IfFa} ]{(e \downarrow \mathtt{false}) }
% {\judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{ \type{\ActS}{\INT}}  \xrightarrow{~\tau~} \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS}{\INT}}}
% \end{array}
% $$
% \caption{Typed LTS (III)\label{t:typedltsiii}}
% \end{table}
